@Article{pavlova06,
  author = 	 {Mariela Pavlova and Lilian Burdy},
  title = 	 {Java Bytecode Specification and Verification},
  journal = 	 {21st Annual ACM Symposium on Applied Computing},
  year = 	 {2006},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {}, 
  OPTpages = 	 {},     
  OPTmonth = 	 {},   
  OPTnote = 	 {},  
  OPTannote = 	 {}    
}   

@Book{hansmann:02,
  author =	"U. Hansmann and M. S. Nicklous and T. Sch{\"{a}}ck and
		 F. Seliger",
  title =	"Smart Card Application Development Using Java",
  publisher =	"Springer-Verlag",
  year = 	"2002",
  isbn_issn =	"3-540-65829-7",
}
    
  
@INPROCEEDINGS{berg:01,
  author = {Joachim van den Berg and Bart Jacobs},
  title = {The {LOOP} Compiler for Java and {JML}},
  booktitle = {TACAS},
  year = {2001},
  editor = {Tiziana Margaria and Wang Yi},
  volume = {2031},
  series = {Lecture Notes in Computer Science},
  pages = {299--312},
  publisher = {Springer},
  bibdate = {2002-01-03},
  bibsource = {DBLP, http://dblp.uni-trier.de/db/conf/tacas/tacas2001.html#BergJ01},
  isbn = {3-540-41865-2},
  url = {http://link.springer.de/link/service/series/0558/bibs/2031/20310299.htm}
}   
  
@TECHREPORT{bhorkar:00,
  author = {Abhay Bhorkar},
  title = {A Run-time Assertion Checker for {Java} using {JML}},
  institution = {Department of Computer Science, Iowa State University},
  year = {2000},
  number = {00-08},
  address = {226 Atanasoff Hall, Ames, Iowa 50011},
  month = may,
  note = {Available by anonymous ftp from ftp.cs.iastate.edu or by e-mail from
	almanac@cs.iastate.edu.},
  key = {Bhorkar},
  url = {ftp://ftp.cs.iastate.edu/pub/techreports/TR00-08/TR.ps.gz}
}
  
@TechReport{ortiz:05,
  author = 	 {Enrique Ortiz},
  title = 	 {An Introduction to Java Card Technology},
  institution =  {Sun},
  year = 	 {2005},
  url = {http://developers.sun.com/techtopics/mobility/javacard/articles/javacard1},
  OPTkey = 	 {},
  OPTtype = 	 {},
  OPTnumber = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@TECHREPORT{oai:CiteSeerPSU:311335,
  author = {Abhay Bhorkar},
  title = {A Run-time Assertion Checker for Java using {JML}},
  year = {2000},
  abstract = {The Java Modeling Language (JML) is a behavioral interface specification
	language tailored for specifying Java modules. This paper describes
	a source-to-source translation tool that takes a JML specification
	and Java source code for a module and produces source code that
	checks assertions at run-time. It describes issues unique to JML,
	including specification-only variables, refinement, specification
	inheritance, and privacy. It also describes the design and implementation
	of the translation tool. Contents 1 Introduction 3 1.1 Specification
	and Assertion Checking ................ . 3 1.2 Goals ............................
	. . 3 1.3 Overview of the tool ...................... . . 4 2 Issues
	7 2.1 JML features ......................... . . 7 2.1.1 Preconditions
	[JML keyword: requires] ............. 7 2.1.2 Assertion Express...},
  annote = {Abhay Bhorkar (Copyright c Iowa State University , 2000);},
  bibsource = {OAI-PMH server at cs1.ist.psu.edu},
  citeseer-references = {oai:CiteSeerPSU:80315; oai:CiteSeerPSU:68287; oai:CiteSeerPSU:361313},
  language = {en},
  oai = {oai:CiteSeerPSU:311335},
  rights = {unrestricted},
  url = {http://citeseer.ist.psu.edu/311335.html; ftp://ftp.cs.iastate.edu/pub/techreports/TR00-08/TR.ps.gz}
}


@ARTICLE{breunesse:04,
  author = {Breunesse and Catano and Huisman and Jacobs},
  title = {Formal Methods for Smart Cards: An Experience Report},
  journal = {SCIPROG: Science of Computer Programming},
  year = {2005},
  volume = {55}
}


@ARTICLE{burdy:05,
  author = {Lilian Burdy and Yoonsik Cheon and David R. Cok and Michael D. Ernst
	and Joseph R. Kiniry and Gary T. Leavens and K. Rustan M. Leino
	and Erik Poll},
  title = {An overview of {JML} tools and applications},
  journal = {Int. J. Softw. Tools Technol. Transf.},
  year = {2005},
  volume = {7},
  pages = {212--232},
  number = {3},
  abstract = {The Java Modeling Language (JML) can be used to specify the detailed
	design of Java classes and interfaces by adding annotations to Java
	source files. The aim of JML is to provide a specification language
	that is easy to use for Java programmers and that is supported by
	a wide range of tools for specification typechecking, runtime debugging,
	static analysis, and verification.This paper gives an overview of
	the main ideas behind JML, details about JML's wide range of tools,
	and a glimpse into existing applications of JML.},
  address = {Berlin, Heidelberg},
  doi = {10.1007/s10009-004-0167-4},
  doi-url = {http://dx.doi.org/10.1007/s10009-004-0167-4},
  publisher = {Springer-Verlag}
}

@BOOK{chen:00,
  title = {{Java Card} technology for {Smart Cards}: architecture and programmer's
	guide},
  publisher = {Ad{\-d}i{\-s}on-Wes{\-l}ey},
  year = {2000},
  author = {Zhiqun Chen},
  pages = {xxii + 368},
  series = {Java series},
  address = {pub-AW:adr},
  acknowledgement = {Nelson H. F. Beebe, University of Utah, Department of Mathematics,
	110 LCB, 155 S 1400 E RM 233, Salt Lake City, UT 84112-0090, USA,
	Tel: +1 801 581 5254, FAX: +1 801 581 4148, e-mail: \path|beebe@math.utah.edu|,
	\path|beebe@acm.org|, \path|beebe@computer.org| (Internet), URL:
	\path|http://www.math.utah.edu/~beebe/|},
  bibdate = {Mon May 6 06:26:30 MDT 2002},
  isbn = {0-201-70329-7},
  isbn-13 = {978-0-201-70329-0},
  keywords = {Java (computer program language); smart cards},
  lccn = {QA76.73.J38 C478 2000}
}
 
@PHDTHESIS{cheon03,    
  author = {Yoonsik Cheon},
  title = {A Runtime Assertion Checker for the {Java Modeling Language}},
  year = {2003},
  month = apr,
  note = {The author's Ph.D. dissertation. Available from \url{archives.cs.iastate.edu}},
  institution = {Department of Computer Science, Iowa State University},
  number = {03-09}
}   

@MISC{eiffel2004a,
  author = {{Eiffel Software}},
  title = {Building Bug-Free {O-O} Software: An Introduction to {D}esign by
	{C}ontract},
  note = {URL: {\urlBiBTeX{http://archive.eiffel.com/doc/manuals/technology/contract/}}},
  url = {http://archive.eiffel.com/doc/manuals/technology/contract/}
}

@INPROCEEDINGS{leino:02,
  author = {Cormac Flanagan and K. Rustan M. Leino and Mark Lillibridge and Greg
	Nelson and James B. Saxe and Raymie Stata},
  title = {Extended Static Checking for Java},
  booktitle = {PLDI},
  year = {2002},
  pages = {234--245},
  bibdate = {2002-12-09},
  bibsource = {DBLP, http://dblp.uni-trier.de/db/conf/pldi/pldi2002.html#FlanaganLLNSS02},
  url = {http://doi.acm.org/10.1145/512529.512558}
}

@BOOK{GutHor93,
  title = {Larch: Languages and Tools for Formal Specification},
  publisher = {Springer-Verlag, Berlin},
  year = {1993},
  author = {J. Guttag and J. Horning},
  keyword = {Larch, Larch/C}
}

@ARTICLE{hubbers:04,
  author = {E. Hubbers and M. Oostdijk and E. Poll},
  title = {Implementing a {Formally Verifiable Security Protocol} in {Java Card}},
  journal = {Lecture Notes in Computer Science},
  year = {2004},
  volume = {2802},
  pages = {213--226},
  acknowledgement = {Nelson H. F. Beebe, University of Utah, Department of Mathematics,
	110 LCB, 155 S 1400 E RM 233, Salt Lake City, UT 84112-0090, USA,
	Tel: +1 801 581 5254, FAX: +1 801 581 4148, e-mail: \path|beebe@math.utah.edu|,
	\path|beebe@acm.org|, \path|beebe@computer.org| (Internet), URL:
	\path|http://www.math.utah.edu/~beebe/|},
  bibdate = {Wed Mar 3 07:11:27 MST 2004},
  bibsource = {Ingenta database},
  coden = {LNCSD9},
  issn = {0302-9743}
}

@INPROCEEDINGS{hubbers:00,
  author = {Engelbert Hubbers and Erik Poll},
  title = {Reasoning about Card Tears and Transactions in Java Card},
  booktitle = {FASE},
  year = {2004},
  editor = {Michel Wermelinger and Tiziana Margaria},
  volume = {2984},
  series = {Lecture Notes in Computer Science},
  pages = {114--128},
  publisher = {Springer},
  bibdate = {2004-03-02},
  bibsource = {DBLP, http://dblp.uni-trier.de/db/conf/fase/fase2004.html#HubbersP04},
  isbn = {3-540-21305-8},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&amp;issn=0302-9743&amp;volume=2984&amp;spage=114}
}

@ARTICLE{meyer:97,
  author = {Jean-Marc J\'{e}z\'{e}quel and Bertrand Meyer},
  title = {Design by Contract: {T}he Lessons of Ariane},
  journal = {IEEE Computer},
  year = {1997},
  volume = {30},
  pages = {129--130},
  number = {1},
  month = jan
}

@INPROCEEDINGS{kiniry,
  author = {Joe Kiniry and Patrice Chalin and Clement Hurlin},
  title = {Integrating Static Checking and Interactive Verification: Supporting
	Multiple Theories and Provers in Verification},
  booktitle = {Proc.\ Verified Software: Theories, Tools, Experiments (VSTTE), Z{\"u}rich},
  year = {2005},
  url = {http://secure.ucd.ie/documents/published/KiniryChalinHurlin05.pdf}
}

@UNPUBLISHED{leavens:06,
  author = {Gary T. Leavens and Yoonsik Cheon},
  title = {Design by Contract with {JML}},
  note = {Draft, available from jmlspecs.org.},
  year = {2006},
  annote = {12 references.},
  key = {Leavens \& Cheon},
  url = {ftp://ftp.cs.iastate.edu/pub/leavens/JML/jmldbc.pdf}
}

@MANUAL{JML-Ref-Manual,
  title = {{JML} Reference Manual},
  author = {Gary T. Leavens and Erik Poll and Curtis Clifton and Yoonsik Cheon
	and Clyde Ruby and David Cok and Peter M{\"u}ller and Joseph Kiniry
	and Patrice Chalin},
  month = may,
  year = {2006},
  note = {Draft revision 1.193},
  key = {JML},
  url = {ftp://ftp.cs.iastate.edu/pub/leavens/JML/jmlrefman.pdf}
}

@BOOK{meyer:91,
  title = {Eiffel: The Language},
  publisher = {Prentice Hall},
  year = {1991},
  editor = {Bertrand Meyer},
  author = {Bertrand Meyer}
}

@ARTICLE{meyer:92,
  author = {Bertrand Meyer},
  title = {Applying Design by Contract},
  journal = {IEEE Computer},
  year = {1992},
  volume = {25},
  pages = {40-51},
  number = {10}
}

@MISC{jc:06,
  author = {Sun Microsystems},
  title = {Java Card Technology Overview},
  howpublished = {<http://java.sun.com/products/javacard/overview.html>},
  year = {Acessado em julho de 2006}
}  
 
@MISC{ortiz:03,
  author = {C. Enrique Ortiz},
  title = {An Introduction to Java Card Technology - Part 2, The Java Card Applet},
  howpublished = {<http://developers.sun.com/techtopics/mobility/javacard/articles/javacard2/>},
  year = {2003, Acessado em outubro de 2006}
}  
  

@ARTICLE{poll01,
  author = {Erik Poll and Joachim van den Berg and Bart Jacobs},
  title = {Formal specification of the JavaCard {API} in {JML}: the {APDU} class},
  journal = {Computer Networks},
  year = {2001},
  volume = {36},  
  pages = {407--421},
  number = {4},
  bibdate = {2003-03-17},
  bibsource = {DBLP, http://dblp.uni-trier.de/db/journals/cn/cn36.html#PollBJ01},
  url = {http://dx.doi.org/10.1016/S1389-1286(01)00163-3}
}   

@INPROCEEDINGS{pool:01,
  author = {Erik Poll and Joachim van den Berg and Bart Jacobs},
  title = {{Specification of the \mbox{JavaCard} API in JML}},
  booktitle = {Smart Card Research and Advanced Application Conference (CARDIS'2000)},
  year = {2000},
  editor = {J. Domingo-Ferrer and D. Chan and A. Watson},
  pages = {135--154},
  publisher = {Kluwer Acad. Publ.}
}             
    
    
@TECHREPORT{Arun:00,    
  author = {Arun D. Raghavan and Gary T. Leavens},
  title = {Desugaring {JML} Method Specifications},
  year = {2000},
  month = aug # {~08},
  abstract = {JML, which stands for {"}Java Modeling Language,{"} is a behavioral
	interface specification language (BISL) designed to specify Java
	modules. JML features a great deal of syntactic sugar that is designed
	to make specifications more expressive. This paper presents a desugaring
	process that boils down all of the syntactic sugars in JML into
	a much simpler form. This desugaring will help one manipulate JML
	specifications in tools, understand the meaning of these sugars,
	and it also allows the use of JML specifications in verification.},
  bibsource = {OAI-PMH server at cs1.ist.psu.edu},
  language = {en},
  oai = {oai:CiteSeerPSU:445167},
  rights = {unrestricted},
  url = {http://citeseer.ist.psu.edu/445167.html; ftp://ftp.cs.iastate.edu/pub/techreports/TR00-03/paper.pdf}
}
 
@MISC{tan03,
  author = {Roy Patrick Tan},
  title = {Runtime Assertion Checking Using {JML}},
  month = aug # {~15},
  year = {2003},
  annote = {Roy Patrick Tan (Department of Computer Science; Virginia Tech; 660
	McBryde Hall , Mail Stop 0106; Blacksburg , VA 24061 , USA);},
  bibsource = {OAI-PMH server at cs1.ist.psu.edu},
  citeseer-references = {oai:CiteSeerPSU:501958; oai:CiteSeerPSU:678031; oai:CiteSeerPSU:68287;
	oai:CiteSeerPSU:311012},
  description = {this paper do not necessarily reflect the views of the NSF},
  language = {en},
  oai = {oai:CiteSeerPSU:680677},
  rights = {unrestricted},
  url = {http://citeseer.ist.psu.edu/680677.html; http://www.cs.iastate.edu/~leavens/SAVCBS/2003/papers/demos/tan.pdf}
}

@MISC{savcbs:03a,
  author = {Roy Patrick Tan and Stephen H. Edwards},
  title = {An Assertion Checking Wrapper Design for Java},
  month = aug # {~15},
  year = {2003},
  abstract = {The Java Modeling Language allows one to write formal behavioral specifications
	for Java classes in structured comments within the source code,
	and then automatically generate run-time assertion checks based
	on such a specification. Instead of placing the generated assertion
	checking code directly in the underlyling class bytecode file, placing
	it is a separate wrapper component o#ers many advantages. Checks
	can be distributed in binary form alongside the compiled class,
	and clients can selectively include or exclude checks on a per-class
	basis without recompilation. In this approach, when checks are excluded
	the underlying code is just as e#cient as if assertions were {"}compiled
	out.{"} In addition, a flexible mechanism for enabling or disabling
	assertion execution on a per-class or per-package basis is also
	included. This paper presents a design for separating assertion
	checking code into wrapper classes and discusses the issues arising
	from this design.},
  annote = {Roy Patrick Tan (Virginia Tech; 660 McBryde Hall , Mail Stop 0106);
	Stephen H. Edwards (Virginia Tech; 660 McBryde Hall , Mail Stop
	0106);},
  bibsource = {OAI-PMH server at cs1.ist.psu.edu},
  citeseer-references = {oai:CiteSeerPSU:612047; oai:CiteSeerPSU:589253; oai:CiteSeerPSU:448240;
	oai:CiteSeerPSU:308299},
  language = {en},
  oai = {oai:CiteSeerPSU:669777},
  rights = {unrestricted},
  url = {http://citeseer.ist.psu.edu/669777.html; http://www.cs.iastate.edu/~leavens/SAVCBS/2003/papers/full-papers/tan-edwards.pdf}
}

@MANUAL{jcre:05,
  title = {Runtime Environment Specification - Java Card Platform, Version 2.2.2},
  organization = {Sun Microsystems},
  year = {2005}
}  

@MANUAL{jcvm:05,
  title = {Virtual Machine Specification - Java Card Platform, Version 2.2.2},
  organization = {Sun Microsystems},
  year = {2005}
}   

@TechReport{escJava:00,
  author =	"K. Rustan M. Leino and Greg Nelson and James B. Saxe",
  title =	"{ESC/Java} User's Manual",
  institution =  "Compaq Systems Research Center",
  year = 	"2000",
  key =  	"Leino \& Nelson \& Saxe",
  type = 	"Technical Note",
  month =	oct,
}   
  
@Article{Meijer:01,
  author =	"Hans Meijer and Erik Poll",
  title =	"Towards a Full Formal Specification of the {JavaCard
		 API}",
  journal =	"Lecture Notes in Computer Science",
  volume =	"2140",
  pages =	"165--??",
  year = 	"2001",
  CODEN =	"LNCSD9",
  ISSN = 	"0302-9743",
  bibdate =	"Sat Feb 2 13:05:42 MST 2002",
  bibsource =	"http://link.springer-ny.com/link/service/series/0558/tocs/t2140.htm",
  URL =  	"http://link.springer-ny.com/link/service/series/0558/bibs/2140/21400165.htm;
		 http://link.springer-ny.com/link/service/series/0558/papers/2140/21400165.pdf",
  acknowledgement = "Nelson H. F. Beebe, Center for Scientific
		 Computing, University of Utah, Department of
		 Mathematics, 110 LCB, 155 S 1400 E RM 233, Salt Lake
		 City, UT 84112-0090, USA, Tel: +1 801 581 5254, FAX: +1
		 801 581 4148, e-mail: \path|beebe@math.utah.edu|,
		 \path|beebe@acm.org|, \path|beebe@computer.org|,
		 \path|beebe@ieee.org| (Internet), URL:
		 \path|http://www.math.utah.edu/~beebe/|",
}

@InProceedings{Cheon-Leavens02,
  key =  	"Cheon \& Leavens",
  author =	"Yoonsik Cheon and Gary T. Leavens",
  title =	"A Simple and Practical Approach to Unit Testing: The
		 {JML} and {JUnit} Way",
  booktitle =	"ECOOP 2002 --- Object-Oriented Programming, 16th
		 European Conference, M\'{a}alaga, Spain, Proceedings",
  pages =	"231--255",
  year = 	"2002",
  editor =	"Boris Magnusson",
  volume =	"2374",
  series =	"Lecture Notes in Computer Science",
  address =	"Berlin",
  month =	jun,
  publisher =	"Springer-Verlag",
  annote =	"The jmlunit tool. 38 references.",
}

@InProceedings{denJac01,
  author =	"van den Berg and Jacobs",
  title =	"The {LOOP} Compiler for Java and {JML}",
  booktitle =	"TACAS: International Workshop on Tools and Algorithms
		 for the Construction and Analysis of Systems, LNCS",
  year = 	"2001",
}

@Article{Shankar:96,
  author =	"N. Shankar",
  title =	"{PVS}: Combining Specification, Proof Checking, and
		 Model Checking",
  journal =	"Lecture Notes in Computer Science",
  volume =	"1166",
  pages =	"257--??",
  year = 	"1996",
  CODEN =	"LNCSD9",
  ISSN = 	"0302-9743",
  bibdate =	"Sat Dec 21 09:47:26 1996",
  acknowledgement = "Nelson H. F. Beebe, Center for Scientific
		 Computing, University of Utah, Department of
		 Mathematics, 110 LCB, 155 S 1400 E RM 233, Salt Lake
		 City, UT 84112-0090, USA, Tel: +1 801 581 5254, FAX: +1
		 801 581 4148, e-mail: \path|beebe@math.utah.edu|,
		 \path|beebe@acm.org|, \path|beebe@computer.org|,
		 \path|beebe@ieee.org| (Internet), URL:
		 \path|http://www.math.utah.edu/~beebe/|",
}

@Article{Marche:04,
  author =	"C. Marche and C. Paulin Mohring and X. Urbain",
  title =	"The {KRAKATOA} tool for certification of {JAVA\slash
		 JAVACARD} programs annotated in {JML}",
  journal =	"Journal of Logic and Algebraic Programming",
  volume =	"58",
  number =	"1--2",
  pages =	"89--106",
  year = 	"2004",
  CODEN =	"????",
  ISSN = 	"1567-8326",
  bibdate =	"Tue Jan 27 06:08:07 MST 2004",
  bibsource =	"Ingenta database",
  acknowledgement = "Nelson H. F. Beebe, University of Utah, Department
		 of Mathematics, 110 LCB, 155 S 1400 E RM 233, Salt Lake
		 City, UT 84112-0090, USA, Tel: +1 801 581 5254, FAX: +1
		 801 581 4148, e-mail: \path|beebe@math.utah.edu|,
		 \path|beebe@acm.org|, \path|beebe@computer.org|
		 (Internet), URL:
		 \path|http://www.math.utah.edu/~beebe/|",
}

@Misc{Coq,
  title =	"The Coq Proof Assistant : Reference Manual : Version
		 7.2",
  author =	"The Coq",
  publisher =	"HAL - CCSd - CNRS",
  year = 	"2002",
  month =	feb,
  abstract =	"Coq is a proof assistant based on a higher-order
		 logic. Coq allows to handle calculus mathematical
		 assertions and to check mechanically proofs of these
		 assertions. It helps to find formal proofs, and allows
		 extraction of a certified program from the constructive
		 proof of its formal specification. This document is the
		 reference manual for the version V7.2 of Coq which is
		 available from http://coq.inria.fr.",
  annote =	"Rapport De Recherche Inria
		 <anne.adolphe@inrialpes.fr>",
  bibsource =	"OAI-PMH server at hal.ccsd.cnrs.fr",
  contributor =  "Rapport De Recherche Inria
		 <anne.adolphe@inrialpes.fr>",
  coverage =	"COQ / PROOF ASSISTANT / FORMAL PROOFS / CALCULUS OF
		 INDUCTIVE CONSTRUCTIONS",
  identifier =	"inria-00069919 (version 1)",
  oai =  	"oai:hal.ccsd.cnrs.fr:inria-00069919_v1",
  subject =	"Computer Science",
  type = 	"RAPPORT",
  URL =  	"http://hal.inria.fr/inria-00069919/en/;
		 http://hal.ccsd.cnrs.fr/docs/00/06/99/19/PDF/RT-0255.pdf",
}  

@Book{Abrial96a,
  author =	"Jean-Raymond Abrial",
  title =	"The {B}~Book: Assigning Programs to Meanings",
  publisher =	"Cambridge University Press",
  isbn_issn =	"0521496195",
  year = 	"1996",
  month =	aug,
}

@Unpublished{ClearSy96,
  key =  	"ClearSy",
  author =	"ClearSy",
  title =	"{Atelier B}, User and Reference Manuals",
  note = 	"\url{http://tinyurl.com/lkj72}",
  year = 	"1996",
}
     
@Book{jurgensen:02,
  author = 	 {Timothy M Jurgensen and Scott B Guthery},
  ALTeditor = 	 {Editor},
  title = 	 {Smart Cards: A Developer's Toolkit},
  publisher = 	 {Prentice Hall PTR},
  year = 	 {2002},
  isbn = 	 {0130937304},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},  
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},  
  OPTnote = 	 {},
  OPTannote = 	 {}
}   

@MastersThesis{burri:05,
  author = 	 {Samuel Burri},
  title = 	 {Design of a Java/Jml Frontend for BoogiePL},
  OPTschool = 	 {School},
  year = 	 {2005},
  OPTkey = 	 {}, 
  OPTtype = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {}, 
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@TechReport{parr:00,
  author = 	 {Terence Parr},
  title = 	 {An Introduction to ANTLR},
  institution =  {Institution},
  year = 	 {2000},
  OPTkey = 	 {},
  OPTtype = 	 {},
  OPTnumber = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}